Left Termination of the query pattern
fib(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 189 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 272 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇒, 8 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇒, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇒, 0 ms)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔, 0 ms)
        ↳27 YES
    ↳28 PiDP
        ↳29 UsableRulesProof (⇔, 0 ms)
        ↳30 PiDP
        ↳31 PiDPToQDPProof (⇒, 0 ms)
        ↳32 QDP
        ↳33 QDPSizeChangeProof (⇔, 0 ms)
        ↳34 YES
    ↳35 PiDP
        ↳36 UsableRulesProof (⇔, 0 ms)
        ↳37 PiDP
        ↳38 PiDPToQDPProof (⇒, 0 ms)
        ↳39 QDP
        ↳40 QDPSizeChangeProof (⇔, 0 ms)
        ↳41 YES

(0) Obligation:

Clauses:

add(0, 0, 0).
add(s(X), Y, s(N)) :- add(X, Y, N).
add(X, s(Y), s(N)) :- add(X, Y, N).
fib(0, 0).
fib(s(0), s(0)).
fib(s(s(X)), N) :- ','(fib(s(X), N1), ','(fib(X, N2), add(N1, N2, N))).

Query: fib(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

addA(s(X1), s(X2)) :- addA(X1, X2).
addB(X1, s(X2)) :- addA(X1, X2).
addB(s(X1), s(X2)) :- addB(X1, X2).
fibC(s(X1), X2) :- pD(X1, X3, X4, X2).
pD(X1, X2, X3, X4) :- fibC(X1, X2).
pD(X1, X2, X3, X4) :- ','(fibcC(X1, X2), fibF(X1, X3)).
pD(X1, X2, X3, X4) :- ','(fibcC(X1, X2), ','(fibcF(X1, X3), addE(X2, X3, X4))).
addE(s(X1), X2, s(X3)) :- addE(X1, X2, X3).
addE(X1, s(X2), s(X3)) :- addE(X1, X2, X3).
fibF(s(s(X1)), X2) :- pD(X1, X3, X4, X2).
addG(s(X1), X2, s(X3)) :- addG(X1, X2, X3).
addG(X1, s(X2), s(X3)) :- addG(X1, X2, X3).
fibI(s(s(0)), X1) :- ','(fibcH(X2), addB(X2, X1)).
fibI(s(s(s(X1))), X2) :- fibC(X1, X3).
fibI(s(s(s(X1))), X2) :- ','(fibcC(X1, X3), fibF(X1, X4)).
fibI(s(s(s(X1))), X2) :- ','(fibcC(X1, X3), ','(fibcF(X1, X4), addE(X3, X4, X5))).
fibI(s(s(s(X1))), X2) :- ','(fibcC(X1, X3), ','(fibcF(X1, X4), ','(addcE(X3, X4, X5), fibC(X1, X6)))).
fibI(s(s(s(X1))), X2) :- ','(fibcC(X1, X3), ','(fibcF(X1, X4), ','(addcE(X3, X4, X5), ','(fibcC(X1, X6), addG(X5, X6, X2))))).

Clauses:

addcA(0, 0).
addcA(s(X1), s(X2)) :- addcA(X1, X2).
addcB(X1, s(X2)) :- addcA(X1, X2).
addcB(s(X1), s(X2)) :- addcB(X1, X2).
fibcC(0, s(0)).
fibcC(s(X1), X2) :- qcD(X1, X3, X4, X2).
qcD(X1, X2, X3, X4) :- ','(fibcC(X1, X2), ','(fibcF(X1, X3), addcE(X2, X3, X4))).
addcE(0, 0, 0).
addcE(s(X1), X2, s(X3)) :- addcE(X1, X2, X3).
addcE(X1, s(X2), s(X3)) :- addcE(X1, X2, X3).
fibcF(0, 0).
fibcF(s(0), s(0)).
fibcF(s(s(X1)), X2) :- qcD(X1, X3, X4, X2).
addcG(0, 0, 0).
addcG(s(X1), X2, s(X3)) :- addcG(X1, X2, X3).
addcG(X1, s(X2), s(X3)) :- addcG(X1, X2, X3).
fibcH(0).

Afs:

fibI(x1, x2)  =  fibI(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
fibI_in: (b,f)
addB_in: (b,f)
addA_in: (b,f)
fibC_in: (b,f)
pD_in: (b,f,f,f)
fibcC_in: (b,f)
qcD_in: (b,f,f,f)
fibcF_in: (b,f)
addcE_in: (b,b,f)
fibF_in: (b,f)
addE_in: (b,b,f)
addG_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

FIBI_IN_GA(s(s(0)), X1) → U15_GA(X1, fibcH_in_a(X2))
U15_GA(X1, fibcH_out_a(X2)) → U16_GA(X1, addB_in_ga(X2, X1))
U15_GA(X1, fibcH_out_a(X2)) → ADDB_IN_GA(X2, X1)
ADDB_IN_GA(X1, s(X2)) → U2_GA(X1, X2, addA_in_ga(X1, X2))
ADDB_IN_GA(X1, s(X2)) → ADDA_IN_GA(X1, X2)
ADDA_IN_GA(s(X1), s(X2)) → U1_GA(X1, X2, addA_in_ga(X1, X2))
ADDA_IN_GA(s(X1), s(X2)) → ADDA_IN_GA(X1, X2)
ADDB_IN_GA(s(X1), s(X2)) → U3_GA(X1, X2, addB_in_ga(X1, X2))
ADDB_IN_GA(s(X1), s(X2)) → ADDB_IN_GA(X1, X2)
FIBI_IN_GA(s(s(s(X1))), X2) → U17_GA(X1, X2, fibC_in_ga(X1, X3))
FIBI_IN_GA(s(s(s(X1))), X2) → FIBC_IN_GA(X1, X3)
FIBC_IN_GA(s(X1), X2) → U4_GA(X1, X2, pD_in_gaaa(X1, X3, X4, X2))
FIBC_IN_GA(s(X1), X2) → PD_IN_GAAA(X1, X3, X4, X2)
PD_IN_GAAA(X1, X2, X3, X4) → U5_GAAA(X1, X2, X3, X4, fibC_in_ga(X1, X2))
PD_IN_GAAA(X1, X2, X3, X4) → FIBC_IN_GA(X1, X2)
PD_IN_GAAA(X1, X2, X3, X4) → U6_GAAA(X1, X2, X3, X4, fibcC_in_ga(X1, X2))
U6_GAAA(X1, X2, X3, X4, fibcC_out_ga(X1, X2)) → U7_GAAA(X1, X2, X3, X4, fibF_in_ga(X1, X3))
U6_GAAA(X1, X2, X3, X4, fibcC_out_ga(X1, X2)) → FIBF_IN_GA(X1, X3)
FIBF_IN_GA(s(s(X1)), X2) → U12_GA(X1, X2, pD_in_gaaa(X1, X3, X4, X2))
FIBF_IN_GA(s(s(X1)), X2) → PD_IN_GAAA(X1, X3, X4, X2)
U6_GAAA(X1, X2, X3, X4, fibcC_out_ga(X1, X2)) → U8_GAAA(X1, X2, X3, X4, fibcF_in_ga(X1, X3))
U8_GAAA(X1, X2, X3, X4, fibcF_out_ga(X1, X3)) → U9_GAAA(X1, X2, X3, X4, addE_in_gga(X2, X3, X4))
U8_GAAA(X1, X2, X3, X4, fibcF_out_ga(X1, X3)) → ADDE_IN_GGA(X2, X3, X4)
ADDE_IN_GGA(s(X1), X2, s(X3)) → U10_GGA(X1, X2, X3, addE_in_gga(X1, X2, X3))
ADDE_IN_GGA(s(X1), X2, s(X3)) → ADDE_IN_GGA(X1, X2, X3)
ADDE_IN_GGA(X1, s(X2), s(X3)) → U11_GGA(X1, X2, X3, addE_in_gga(X1, X2, X3))
ADDE_IN_GGA(X1, s(X2), s(X3)) → ADDE_IN_GGA(X1, X2, X3)
FIBI_IN_GA(s(s(s(X1))), X2) → U18_GA(X1, X2, fibcC_in_ga(X1, X3))
U18_GA(X1, X2, fibcC_out_ga(X1, X3)) → U19_GA(X1, X2, fibF_in_ga(X1, X4))
U18_GA(X1, X2, fibcC_out_ga(X1, X3)) → FIBF_IN_GA(X1, X4)
U18_GA(X1, X2, fibcC_out_ga(X1, X3)) → U20_GA(X1, X2, X3, fibcF_in_ga(X1, X4))
U20_GA(X1, X2, X3, fibcF_out_ga(X1, X4)) → U21_GA(X1, X2, addE_in_gga(X3, X4, X5))
U20_GA(X1, X2, X3, fibcF_out_ga(X1, X4)) → ADDE_IN_GGA(X3, X4, X5)
U20_GA(X1, X2, X3, fibcF_out_ga(X1, X4)) → U22_GA(X1, X2, addcE_in_gga(X3, X4, X5))
U22_GA(X1, X2, addcE_out_gga(X3, X4, X5)) → U23_GA(X1, X2, fibC_in_ga(X1, X6))
U22_GA(X1, X2, addcE_out_gga(X3, X4, X5)) → FIBC_IN_GA(X1, X6)
U22_GA(X1, X2, addcE_out_gga(X3, X4, X5)) → U24_GA(X1, X2, X5, fibcC_in_ga(X1, X6))
U24_GA(X1, X2, X5, fibcC_out_ga(X1, X6)) → U25_GA(X1, X2, addG_in_gga(X5, X6, X2))
U24_GA(X1, X2, X5, fibcC_out_ga(X1, X6)) → ADDG_IN_GGA(X5, X6, X2)
ADDG_IN_GGA(s(X1), X2, s(X3)) → U13_GGA(X1, X2, X3, addG_in_gga(X1, X2, X3))
ADDG_IN_GGA(s(X1), X2, s(X3)) → ADDG_IN_GGA(X1, X2, X3)
ADDG_IN_GGA(X1, s(X2), s(X3)) → U14_GGA(X1, X2, X3, addG_in_gga(X1, X2, X3))
ADDG_IN_GGA(X1, s(X2), s(X3)) → ADDG_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

fibcH_in_a(0) → fibcH_out_a(0)
fibcC_in_ga(0, s(0)) → fibcC_out_ga(0, s(0))
fibcC_in_ga(s(X1), X2) → U30_ga(X1, X2, qcD_in_gaaa(X1, X3, X4, X2))
qcD_in_gaaa(X1, X2, X3, X4) → U31_gaaa(X1, X2, X3, X4, fibcC_in_ga(X1, X2))
U31_gaaa(X1, X2, X3, X4, fibcC_out_ga(X1, X2)) → U32_gaaa(X1, X2, X3, X4, fibcF_in_ga(X1, X3))
fibcF_in_ga(0, 0) → fibcF_out_ga(0, 0)
fibcF_in_ga(s(0), s(0)) → fibcF_out_ga(s(0), s(0))
fibcF_in_ga(s(s(X1)), X2) → U36_ga(X1, X2, qcD_in_gaaa(X1, X3, X4, X2))
U36_ga(X1, X2, qcD_out_gaaa(X1, X3, X4, X2)) → fibcF_out_ga(s(s(X1)), X2)
U32_gaaa(X1, X2, X3, X4, fibcF_out_ga(X1, X3)) → U33_gaaa(X1, X2, X3, X4, addcE_in_gga(X2, X3, X4))
addcE_in_gga(0, 0, 0) → addcE_out_gga(0, 0, 0)
addcE_in_gga(s(X1), X2, s(X3)) → U34_gga(X1, X2, X3, addcE_in_gga(X1, X2, X3))
addcE_in_gga(X1, s(X2), s(X3)) → U35_gga(X1, X2, X3, addcE_in_gga(X1, X2, X3))
U35_gga(X1, X2, X3, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(X1, s(X2), s(X3))
U34_gga(X1, X2, X3, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(s(X1), X2, s(X3))
U33_gaaa(X1, X2, X3, X4, addcE_out_gga(X2, X3, X4)) → qcD_out_gaaa(X1, X2, X3, X4)
U30_ga(X1, X2, qcD_out_gaaa(X1, X3, X4, X2)) → fibcC_out_ga(s(X1), X2)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
fibcH_in_a(x1)  =  fibcH_in_a
fibcH_out_a(x1)  =  fibcH_out_a(x1)
addB_in_ga(x1, x2)  =  addB_in_ga(x1)
addA_in_ga(x1, x2)  =  addA_in_ga(x1)
fibC_in_ga(x1, x2)  =  fibC_in_ga(x1)
pD_in_gaaa(x1, x2, x3, x4)  =  pD_in_gaaa(x1)
fibcC_in_ga(x1, x2)  =  fibcC_in_ga(x1)
fibcC_out_ga(x1, x2)  =  fibcC_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
qcD_in_gaaa(x1, x2, x3, x4)  =  qcD_in_gaaa(x1)
U31_gaaa(x1, x2, x3, x4, x5)  =  U31_gaaa(x1, x5)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x2, x5)
fibcF_in_ga(x1, x2)  =  fibcF_in_ga(x1)
fibcF_out_ga(x1, x2)  =  fibcF_out_ga(x1, x2)
U36_ga(x1, x2, x3)  =  U36_ga(x1, x3)
qcD_out_gaaa(x1, x2, x3, x4)  =  qcD_out_gaaa(x1, x2, x3, x4)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x2, x3, x5)
addcE_in_gga(x1, x2, x3)  =  addcE_in_gga(x1, x2)
addcE_out_gga(x1, x2, x3)  =  addcE_out_gga(x1, x2, x3)
U34_gga(x1, x2, x3, x4)  =  U34_gga(x1, x2, x4)
U35_gga(x1, x2, x3, x4)  =  U35_gga(x1, x2, x4)
fibF_in_ga(x1, x2)  =  fibF_in_ga(x1)
addE_in_gga(x1, x2, x3)  =  addE_in_gga(x1, x2)
addG_in_gga(x1, x2, x3)  =  addG_in_gga(x1, x2)
FIBI_IN_GA(x1, x2)  =  FIBI_IN_GA(x1)
U15_GA(x1, x2)  =  U15_GA(x2)
U16_GA(x1, x2)  =  U16_GA(x2)
ADDB_IN_GA(x1, x2)  =  ADDB_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
ADDA_IN_GA(x1, x2)  =  ADDA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U17_GA(x1, x2, x3)  =  U17_GA(x1, x3)
FIBC_IN_GA(x1, x2)  =  FIBC_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
PD_IN_GAAA(x1, x2, x3, x4)  =  PD_IN_GAAA(x1)
U5_GAAA(x1, x2, x3, x4, x5)  =  U5_GAAA(x1, x5)
U6_GAAA(x1, x2, x3, x4, x5)  =  U6_GAAA(x1, x5)
U7_GAAA(x1, x2, x3, x4, x5)  =  U7_GAAA(x1, x5)
FIBF_IN_GA(x1, x2)  =  FIBF_IN_GA(x1)
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
U8_GAAA(x1, x2, x3, x4, x5)  =  U8_GAAA(x1, x2, x5)
U9_GAAA(x1, x2, x3, x4, x5)  =  U9_GAAA(x1, x5)
ADDE_IN_GGA(x1, x2, x3)  =  ADDE_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U18_GA(x1, x2, x3)  =  U18_GA(x1, x3)
U19_GA(x1, x2, x3)  =  U19_GA(x1, x3)
U20_GA(x1, x2, x3, x4)  =  U20_GA(x1, x3, x4)
U21_GA(x1, x2, x3)  =  U21_GA(x1, x3)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
U23_GA(x1, x2, x3)  =  U23_GA(x1, x3)
U24_GA(x1, x2, x3, x4)  =  U24_GA(x1, x3, x4)
U25_GA(x1, x2, x3)  =  U25_GA(x1, x3)
ADDG_IN_GGA(x1, x2, x3)  =  ADDG_IN_GGA(x1, x2)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)
U14_GGA(x1, x2, x3, x4)  =  U14_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FIBI_IN_GA(s(s(0)), X1) → U15_GA(X1, fibcH_in_a(X2))
U15_GA(X1, fibcH_out_a(X2)) → U16_GA(X1, addB_in_ga(X2, X1))
U15_GA(X1, fibcH_out_a(X2)) → ADDB_IN_GA(X2, X1)
ADDB_IN_GA(X1, s(X2)) → U2_GA(X1, X2, addA_in_ga(X1, X2))
ADDB_IN_GA(X1, s(X2)) → ADDA_IN_GA(X1, X2)
ADDA_IN_GA(s(X1), s(X2)) → U1_GA(X1, X2, addA_in_ga(X1, X2))
ADDA_IN_GA(s(X1), s(X2)) → ADDA_IN_GA(X1, X2)
ADDB_IN_GA(s(X1), s(X2)) → U3_GA(X1, X2, addB_in_ga(X1, X2))
ADDB_IN_GA(s(X1), s(X2)) → ADDB_IN_GA(X1, X2)
FIBI_IN_GA(s(s(s(X1))), X2) → U17_GA(X1, X2, fibC_in_ga(X1, X3))
FIBI_IN_GA(s(s(s(X1))), X2) → FIBC_IN_GA(X1, X3)
FIBC_IN_GA(s(X1), X2) → U4_GA(X1, X2, pD_in_gaaa(X1, X3, X4, X2))
FIBC_IN_GA(s(X1), X2) → PD_IN_GAAA(X1, X3, X4, X2)
PD_IN_GAAA(X1, X2, X3, X4) → U5_GAAA(X1, X2, X3, X4, fibC_in_ga(X1, X2))
PD_IN_GAAA(X1, X2, X3, X4) → FIBC_IN_GA(X1, X2)
PD_IN_GAAA(X1, X2, X3, X4) → U6_GAAA(X1, X2, X3, X4, fibcC_in_ga(X1, X2))
U6_GAAA(X1, X2, X3, X4, fibcC_out_ga(X1, X2)) → U7_GAAA(X1, X2, X3, X4, fibF_in_ga(X1, X3))
U6_GAAA(X1, X2, X3, X4, fibcC_out_ga(X1, X2)) → FIBF_IN_GA(X1, X3)
FIBF_IN_GA(s(s(X1)), X2) → U12_GA(X1, X2, pD_in_gaaa(X1, X3, X4, X2))
FIBF_IN_GA(s(s(X1)), X2) → PD_IN_GAAA(X1, X3, X4, X2)
U6_GAAA(X1, X2, X3, X4, fibcC_out_ga(X1, X2)) → U8_GAAA(X1, X2, X3, X4, fibcF_in_ga(X1, X3))
U8_GAAA(X1, X2, X3, X4, fibcF_out_ga(X1, X3)) → U9_GAAA(X1, X2, X3, X4, addE_in_gga(X2, X3, X4))
U8_GAAA(X1, X2, X3, X4, fibcF_out_ga(X1, X3)) → ADDE_IN_GGA(X2, X3, X4)
ADDE_IN_GGA(s(X1), X2, s(X3)) → U10_GGA(X1, X2, X3, addE_in_gga(X1, X2, X3))
ADDE_IN_GGA(s(X1), X2, s(X3)) → ADDE_IN_GGA(X1, X2, X3)
ADDE_IN_GGA(X1, s(X2), s(X3)) → U11_GGA(X1, X2, X3, addE_in_gga(X1, X2, X3))
ADDE_IN_GGA(X1, s(X2), s(X3)) → ADDE_IN_GGA(X1, X2, X3)
FIBI_IN_GA(s(s(s(X1))), X2) → U18_GA(X1, X2, fibcC_in_ga(X1, X3))
U18_GA(X1, X2, fibcC_out_ga(X1, X3)) → U19_GA(X1, X2, fibF_in_ga(X1, X4))
U18_GA(X1, X2, fibcC_out_ga(X1, X3)) → FIBF_IN_GA(X1, X4)
U18_GA(X1, X2, fibcC_out_ga(X1, X3)) → U20_GA(X1, X2, X3, fibcF_in_ga(X1, X4))
U20_GA(X1, X2, X3, fibcF_out_ga(X1, X4)) → U21_GA(X1, X2, addE_in_gga(X3, X4, X5))
U20_GA(X1, X2, X3, fibcF_out_ga(X1, X4)) → ADDE_IN_GGA(X3, X4, X5)
U20_GA(X1, X2, X3, fibcF_out_ga(X1, X4)) → U22_GA(X1, X2, addcE_in_gga(X3, X4, X5))
U22_GA(X1, X2, addcE_out_gga(X3, X4, X5)) → U23_GA(X1, X2, fibC_in_ga(X1, X6))
U22_GA(X1, X2, addcE_out_gga(X3, X4, X5)) → FIBC_IN_GA(X1, X6)
U22_GA(X1, X2, addcE_out_gga(X3, X4, X5)) → U24_GA(X1, X2, X5, fibcC_in_ga(X1, X6))
U24_GA(X1, X2, X5, fibcC_out_ga(X1, X6)) → U25_GA(X1, X2, addG_in_gga(X5, X6, X2))
U24_GA(X1, X2, X5, fibcC_out_ga(X1, X6)) → ADDG_IN_GGA(X5, X6, X2)
ADDG_IN_GGA(s(X1), X2, s(X3)) → U13_GGA(X1, X2, X3, addG_in_gga(X1, X2, X3))
ADDG_IN_GGA(s(X1), X2, s(X3)) → ADDG_IN_GGA(X1, X2, X3)
ADDG_IN_GGA(X1, s(X2), s(X3)) → U14_GGA(X1, X2, X3, addG_in_gga(X1, X2, X3))
ADDG_IN_GGA(X1, s(X2), s(X3)) → ADDG_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

fibcH_in_a(0) → fibcH_out_a(0)
fibcC_in_ga(0, s(0)) → fibcC_out_ga(0, s(0))
fibcC_in_ga(s(X1), X2) → U30_ga(X1, X2, qcD_in_gaaa(X1, X3, X4, X2))
qcD_in_gaaa(X1, X2, X3, X4) → U31_gaaa(X1, X2, X3, X4, fibcC_in_ga(X1, X2))
U31_gaaa(X1, X2, X3, X4, fibcC_out_ga(X1, X2)) → U32_gaaa(X1, X2, X3, X4, fibcF_in_ga(X1, X3))
fibcF_in_ga(0, 0) → fibcF_out_ga(0, 0)
fibcF_in_ga(s(0), s(0)) → fibcF_out_ga(s(0), s(0))
fibcF_in_ga(s(s(X1)), X2) → U36_ga(X1, X2, qcD_in_gaaa(X1, X3, X4, X2))
U36_ga(X1, X2, qcD_out_gaaa(X1, X3, X4, X2)) → fibcF_out_ga(s(s(X1)), X2)
U32_gaaa(X1, X2, X3, X4, fibcF_out_ga(X1, X3)) → U33_gaaa(X1, X2, X3, X4, addcE_in_gga(X2, X3, X4))
addcE_in_gga(0, 0, 0) → addcE_out_gga(0, 0, 0)
addcE_in_gga(s(X1), X2, s(X3)) → U34_gga(X1, X2, X3, addcE_in_gga(X1, X2, X3))
addcE_in_gga(X1, s(X2), s(X3)) → U35_gga(X1, X2, X3, addcE_in_gga(X1, X2, X3))
U35_gga(X1, X2, X3, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(X1, s(X2), s(X3))
U34_gga(X1, X2, X3, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(s(X1), X2, s(X3))
U33_gaaa(X1, X2, X3, X4, addcE_out_gga(X2, X3, X4)) → qcD_out_gaaa(X1, X2, X3, X4)
U30_ga(X1, X2, qcD_out_gaaa(X1, X3, X4, X2)) → fibcC_out_ga(s(X1), X2)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
fibcH_in_a(x1)  =  fibcH_in_a
fibcH_out_a(x1)  =  fibcH_out_a(x1)
addB_in_ga(x1, x2)  =  addB_in_ga(x1)
addA_in_ga(x1, x2)  =  addA_in_ga(x1)
fibC_in_ga(x1, x2)  =  fibC_in_ga(x1)
pD_in_gaaa(x1, x2, x3, x4)  =  pD_in_gaaa(x1)
fibcC_in_ga(x1, x2)  =  fibcC_in_ga(x1)
fibcC_out_ga(x1, x2)  =  fibcC_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
qcD_in_gaaa(x1, x2, x3, x4)  =  qcD_in_gaaa(x1)
U31_gaaa(x1, x2, x3, x4, x5)  =  U31_gaaa(x1, x5)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x2, x5)
fibcF_in_ga(x1, x2)  =  fibcF_in_ga(x1)
fibcF_out_ga(x1, x2)  =  fibcF_out_ga(x1, x2)
U36_ga(x1, x2, x3)  =  U36_ga(x1, x3)
qcD_out_gaaa(x1, x2, x3, x4)  =  qcD_out_gaaa(x1, x2, x3, x4)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x2, x3, x5)
addcE_in_gga(x1, x2, x3)  =  addcE_in_gga(x1, x2)
addcE_out_gga(x1, x2, x3)  =  addcE_out_gga(x1, x2, x3)
U34_gga(x1, x2, x3, x4)  =  U34_gga(x1, x2, x4)
U35_gga(x1, x2, x3, x4)  =  U35_gga(x1, x2, x4)
fibF_in_ga(x1, x2)  =  fibF_in_ga(x1)
addE_in_gga(x1, x2, x3)  =  addE_in_gga(x1, x2)
addG_in_gga(x1, x2, x3)  =  addG_in_gga(x1, x2)
FIBI_IN_GA(x1, x2)  =  FIBI_IN_GA(x1)
U15_GA(x1, x2)  =  U15_GA(x2)
U16_GA(x1, x2)  =  U16_GA(x2)
ADDB_IN_GA(x1, x2)  =  ADDB_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
ADDA_IN_GA(x1, x2)  =  ADDA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U17_GA(x1, x2, x3)  =  U17_GA(x1, x3)
FIBC_IN_GA(x1, x2)  =  FIBC_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
PD_IN_GAAA(x1, x2, x3, x4)  =  PD_IN_GAAA(x1)
U5_GAAA(x1, x2, x3, x4, x5)  =  U5_GAAA(x1, x5)
U6_GAAA(x1, x2, x3, x4, x5)  =  U6_GAAA(x1, x5)
U7_GAAA(x1, x2, x3, x4, x5)  =  U7_GAAA(x1, x5)
FIBF_IN_GA(x1, x2)  =  FIBF_IN_GA(x1)
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
U8_GAAA(x1, x2, x3, x4, x5)  =  U8_GAAA(x1, x2, x5)
U9_GAAA(x1, x2, x3, x4, x5)  =  U9_GAAA(x1, x5)
ADDE_IN_GGA(x1, x2, x3)  =  ADDE_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U18_GA(x1, x2, x3)  =  U18_GA(x1, x3)
U19_GA(x1, x2, x3)  =  U19_GA(x1, x3)
U20_GA(x1, x2, x3, x4)  =  U20_GA(x1, x3, x4)
U21_GA(x1, x2, x3)  =  U21_GA(x1, x3)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
U23_GA(x1, x2, x3)  =  U23_GA(x1, x3)
U24_GA(x1, x2, x3, x4)  =  U24_GA(x1, x3, x4)
U25_GA(x1, x2, x3)  =  U25_GA(x1, x3)
ADDG_IN_GGA(x1, x2, x3)  =  ADDG_IN_GGA(x1, x2)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)
U14_GGA(x1, x2, x3, x4)  =  U14_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 32 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDG_IN_GGA(X1, s(X2), s(X3)) → ADDG_IN_GGA(X1, X2, X3)
ADDG_IN_GGA(s(X1), X2, s(X3)) → ADDG_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

fibcH_in_a(0) → fibcH_out_a(0)
fibcC_in_ga(0, s(0)) → fibcC_out_ga(0, s(0))
fibcC_in_ga(s(X1), X2) → U30_ga(X1, X2, qcD_in_gaaa(X1, X3, X4, X2))
qcD_in_gaaa(X1, X2, X3, X4) → U31_gaaa(X1, X2, X3, X4, fibcC_in_ga(X1, X2))
U31_gaaa(X1, X2, X3, X4, fibcC_out_ga(X1, X2)) → U32_gaaa(X1, X2, X3, X4, fibcF_in_ga(X1, X3))
fibcF_in_ga(0, 0) → fibcF_out_ga(0, 0)
fibcF_in_ga(s(0), s(0)) → fibcF_out_ga(s(0), s(0))
fibcF_in_ga(s(s(X1)), X2) → U36_ga(X1, X2, qcD_in_gaaa(X1, X3, X4, X2))
U36_ga(X1, X2, qcD_out_gaaa(X1, X3, X4, X2)) → fibcF_out_ga(s(s(X1)), X2)
U32_gaaa(X1, X2, X3, X4, fibcF_out_ga(X1, X3)) → U33_gaaa(X1, X2, X3, X4, addcE_in_gga(X2, X3, X4))
addcE_in_gga(0, 0, 0) → addcE_out_gga(0, 0, 0)
addcE_in_gga(s(X1), X2, s(X3)) → U34_gga(X1, X2, X3, addcE_in_gga(X1, X2, X3))
addcE_in_gga(X1, s(X2), s(X3)) → U35_gga(X1, X2, X3, addcE_in_gga(X1, X2, X3))
U35_gga(X1, X2, X3, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(X1, s(X2), s(X3))
U34_gga(X1, X2, X3, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(s(X1), X2, s(X3))
U33_gaaa(X1, X2, X3, X4, addcE_out_gga(X2, X3, X4)) → qcD_out_gaaa(X1, X2, X3, X4)
U30_ga(X1, X2, qcD_out_gaaa(X1, X3, X4, X2)) → fibcC_out_ga(s(X1), X2)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
fibcH_in_a(x1)  =  fibcH_in_a
fibcH_out_a(x1)  =  fibcH_out_a(x1)
fibcC_in_ga(x1, x2)  =  fibcC_in_ga(x1)
fibcC_out_ga(x1, x2)  =  fibcC_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
qcD_in_gaaa(x1, x2, x3, x4)  =  qcD_in_gaaa(x1)
U31_gaaa(x1, x2, x3, x4, x5)  =  U31_gaaa(x1, x5)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x2, x5)
fibcF_in_ga(x1, x2)  =  fibcF_in_ga(x1)
fibcF_out_ga(x1, x2)  =  fibcF_out_ga(x1, x2)
U36_ga(x1, x2, x3)  =  U36_ga(x1, x3)
qcD_out_gaaa(x1, x2, x3, x4)  =  qcD_out_gaaa(x1, x2, x3, x4)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x2, x3, x5)
addcE_in_gga(x1, x2, x3)  =  addcE_in_gga(x1, x2)
addcE_out_gga(x1, x2, x3)  =  addcE_out_gga(x1, x2, x3)
U34_gga(x1, x2, x3, x4)  =  U34_gga(x1, x2, x4)
U35_gga(x1, x2, x3, x4)  =  U35_gga(x1, x2, x4)
ADDG_IN_GGA(x1, x2, x3)  =  ADDG_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDG_IN_GGA(X1, s(X2), s(X3)) → ADDG_IN_GGA(X1, X2, X3)
ADDG_IN_GGA(s(X1), X2, s(X3)) → ADDG_IN_GGA(X1, X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ADDG_IN_GGA(x1, x2, x3)  =  ADDG_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ADDG_IN_GGA(X1, s(X2)) → ADDG_IN_GGA(X1, X2)
ADDG_IN_GGA(s(X1), X2) → ADDG_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • ADDG_IN_GGA(X1, s(X2)) → ADDG_IN_GGA(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

  • ADDG_IN_GGA(s(X1), X2) → ADDG_IN_GGA(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDE_IN_GGA(X1, s(X2), s(X3)) → ADDE_IN_GGA(X1, X2, X3)
ADDE_IN_GGA(s(X1), X2, s(X3)) → ADDE_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

fibcH_in_a(0) → fibcH_out_a(0)
fibcC_in_ga(0, s(0)) → fibcC_out_ga(0, s(0))
fibcC_in_ga(s(X1), X2) → U30_ga(X1, X2, qcD_in_gaaa(X1, X3, X4, X2))
qcD_in_gaaa(X1, X2, X3, X4) → U31_gaaa(X1, X2, X3, X4, fibcC_in_ga(X1, X2))
U31_gaaa(X1, X2, X3, X4, fibcC_out_ga(X1, X2)) → U32_gaaa(X1, X2, X3, X4, fibcF_in_ga(X1, X3))
fibcF_in_ga(0, 0) → fibcF_out_ga(0, 0)
fibcF_in_ga(s(0), s(0)) → fibcF_out_ga(s(0), s(0))
fibcF_in_ga(s(s(X1)), X2) → U36_ga(X1, X2, qcD_in_gaaa(X1, X3, X4, X2))
U36_ga(X1, X2, qcD_out_gaaa(X1, X3, X4, X2)) → fibcF_out_ga(s(s(X1)), X2)
U32_gaaa(X1, X2, X3, X4, fibcF_out_ga(X1, X3)) → U33_gaaa(X1, X2, X3, X4, addcE_in_gga(X2, X3, X4))
addcE_in_gga(0, 0, 0) → addcE_out_gga(0, 0, 0)
addcE_in_gga(s(X1), X2, s(X3)) → U34_gga(X1, X2, X3, addcE_in_gga(X1, X2, X3))
addcE_in_gga(X1, s(X2), s(X3)) → U35_gga(X1, X2, X3, addcE_in_gga(X1, X2, X3))
U35_gga(X1, X2, X3, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(X1, s(X2), s(X3))
U34_gga(X1, X2, X3, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(s(X1), X2, s(X3))
U33_gaaa(X1, X2, X3, X4, addcE_out_gga(X2, X3, X4)) → qcD_out_gaaa(X1, X2, X3, X4)
U30_ga(X1, X2, qcD_out_gaaa(X1, X3, X4, X2)) → fibcC_out_ga(s(X1), X2)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
fibcH_in_a(x1)  =  fibcH_in_a
fibcH_out_a(x1)  =  fibcH_out_a(x1)
fibcC_in_ga(x1, x2)  =  fibcC_in_ga(x1)
fibcC_out_ga(x1, x2)  =  fibcC_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
qcD_in_gaaa(x1, x2, x3, x4)  =  qcD_in_gaaa(x1)
U31_gaaa(x1, x2, x3, x4, x5)  =  U31_gaaa(x1, x5)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x2, x5)
fibcF_in_ga(x1, x2)  =  fibcF_in_ga(x1)
fibcF_out_ga(x1, x2)  =  fibcF_out_ga(x1, x2)
U36_ga(x1, x2, x3)  =  U36_ga(x1, x3)
qcD_out_gaaa(x1, x2, x3, x4)  =  qcD_out_gaaa(x1, x2, x3, x4)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x2, x3, x5)
addcE_in_gga(x1, x2, x3)  =  addcE_in_gga(x1, x2)
addcE_out_gga(x1, x2, x3)  =  addcE_out_gga(x1, x2, x3)
U34_gga(x1, x2, x3, x4)  =  U34_gga(x1, x2, x4)
U35_gga(x1, x2, x3, x4)  =  U35_gga(x1, x2, x4)
ADDE_IN_GGA(x1, x2, x3)  =  ADDE_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDE_IN_GGA(X1, s(X2), s(X3)) → ADDE_IN_GGA(X1, X2, X3)
ADDE_IN_GGA(s(X1), X2, s(X3)) → ADDE_IN_GGA(X1, X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ADDE_IN_GGA(x1, x2, x3)  =  ADDE_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ADDE_IN_GGA(X1, s(X2)) → ADDE_IN_GGA(X1, X2)
ADDE_IN_GGA(s(X1), X2) → ADDE_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • ADDE_IN_GGA(X1, s(X2)) → ADDE_IN_GGA(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

  • ADDE_IN_GGA(s(X1), X2) → ADDE_IN_GGA(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FIBC_IN_GA(s(X1), X2) → PD_IN_GAAA(X1, X3, X4, X2)
PD_IN_GAAA(X1, X2, X3, X4) → FIBC_IN_GA(X1, X2)
PD_IN_GAAA(X1, X2, X3, X4) → U6_GAAA(X1, X2, X3, X4, fibcC_in_ga(X1, X2))
U6_GAAA(X1, X2, X3, X4, fibcC_out_ga(X1, X2)) → FIBF_IN_GA(X1, X3)
FIBF_IN_GA(s(s(X1)), X2) → PD_IN_GAAA(X1, X3, X4, X2)

The TRS R consists of the following rules:

fibcH_in_a(0) → fibcH_out_a(0)
fibcC_in_ga(0, s(0)) → fibcC_out_ga(0, s(0))
fibcC_in_ga(s(X1), X2) → U30_ga(X1, X2, qcD_in_gaaa(X1, X3, X4, X2))
qcD_in_gaaa(X1, X2, X3, X4) → U31_gaaa(X1, X2, X3, X4, fibcC_in_ga(X1, X2))
U31_gaaa(X1, X2, X3, X4, fibcC_out_ga(X1, X2)) → U32_gaaa(X1, X2, X3, X4, fibcF_in_ga(X1, X3))
fibcF_in_ga(0, 0) → fibcF_out_ga(0, 0)
fibcF_in_ga(s(0), s(0)) → fibcF_out_ga(s(0), s(0))
fibcF_in_ga(s(s(X1)), X2) → U36_ga(X1, X2, qcD_in_gaaa(X1, X3, X4, X2))
U36_ga(X1, X2, qcD_out_gaaa(X1, X3, X4, X2)) → fibcF_out_ga(s(s(X1)), X2)
U32_gaaa(X1, X2, X3, X4, fibcF_out_ga(X1, X3)) → U33_gaaa(X1, X2, X3, X4, addcE_in_gga(X2, X3, X4))
addcE_in_gga(0, 0, 0) → addcE_out_gga(0, 0, 0)
addcE_in_gga(s(X1), X2, s(X3)) → U34_gga(X1, X2, X3, addcE_in_gga(X1, X2, X3))
addcE_in_gga(X1, s(X2), s(X3)) → U35_gga(X1, X2, X3, addcE_in_gga(X1, X2, X3))
U35_gga(X1, X2, X3, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(X1, s(X2), s(X3))
U34_gga(X1, X2, X3, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(s(X1), X2, s(X3))
U33_gaaa(X1, X2, X3, X4, addcE_out_gga(X2, X3, X4)) → qcD_out_gaaa(X1, X2, X3, X4)
U30_ga(X1, X2, qcD_out_gaaa(X1, X3, X4, X2)) → fibcC_out_ga(s(X1), X2)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
fibcH_in_a(x1)  =  fibcH_in_a
fibcH_out_a(x1)  =  fibcH_out_a(x1)
fibcC_in_ga(x1, x2)  =  fibcC_in_ga(x1)
fibcC_out_ga(x1, x2)  =  fibcC_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
qcD_in_gaaa(x1, x2, x3, x4)  =  qcD_in_gaaa(x1)
U31_gaaa(x1, x2, x3, x4, x5)  =  U31_gaaa(x1, x5)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x2, x5)
fibcF_in_ga(x1, x2)  =  fibcF_in_ga(x1)
fibcF_out_ga(x1, x2)  =  fibcF_out_ga(x1, x2)
U36_ga(x1, x2, x3)  =  U36_ga(x1, x3)
qcD_out_gaaa(x1, x2, x3, x4)  =  qcD_out_gaaa(x1, x2, x3, x4)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x2, x3, x5)
addcE_in_gga(x1, x2, x3)  =  addcE_in_gga(x1, x2)
addcE_out_gga(x1, x2, x3)  =  addcE_out_gga(x1, x2, x3)
U34_gga(x1, x2, x3, x4)  =  U34_gga(x1, x2, x4)
U35_gga(x1, x2, x3, x4)  =  U35_gga(x1, x2, x4)
FIBC_IN_GA(x1, x2)  =  FIBC_IN_GA(x1)
PD_IN_GAAA(x1, x2, x3, x4)  =  PD_IN_GAAA(x1)
U6_GAAA(x1, x2, x3, x4, x5)  =  U6_GAAA(x1, x5)
FIBF_IN_GA(x1, x2)  =  FIBF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FIBC_IN_GA(s(X1), X2) → PD_IN_GAAA(X1, X3, X4, X2)
PD_IN_GAAA(X1, X2, X3, X4) → FIBC_IN_GA(X1, X2)
PD_IN_GAAA(X1, X2, X3, X4) → U6_GAAA(X1, X2, X3, X4, fibcC_in_ga(X1, X2))
U6_GAAA(X1, X2, X3, X4, fibcC_out_ga(X1, X2)) → FIBF_IN_GA(X1, X3)
FIBF_IN_GA(s(s(X1)), X2) → PD_IN_GAAA(X1, X3, X4, X2)

The TRS R consists of the following rules:

fibcC_in_ga(0, s(0)) → fibcC_out_ga(0, s(0))
fibcC_in_ga(s(X1), X2) → U30_ga(X1, X2, qcD_in_gaaa(X1, X3, X4, X2))
U30_ga(X1, X2, qcD_out_gaaa(X1, X3, X4, X2)) → fibcC_out_ga(s(X1), X2)
qcD_in_gaaa(X1, X2, X3, X4) → U31_gaaa(X1, X2, X3, X4, fibcC_in_ga(X1, X2))
U31_gaaa(X1, X2, X3, X4, fibcC_out_ga(X1, X2)) → U32_gaaa(X1, X2, X3, X4, fibcF_in_ga(X1, X3))
U32_gaaa(X1, X2, X3, X4, fibcF_out_ga(X1, X3)) → U33_gaaa(X1, X2, X3, X4, addcE_in_gga(X2, X3, X4))
fibcF_in_ga(0, 0) → fibcF_out_ga(0, 0)
fibcF_in_ga(s(0), s(0)) → fibcF_out_ga(s(0), s(0))
fibcF_in_ga(s(s(X1)), X2) → U36_ga(X1, X2, qcD_in_gaaa(X1, X3, X4, X2))
U33_gaaa(X1, X2, X3, X4, addcE_out_gga(X2, X3, X4)) → qcD_out_gaaa(X1, X2, X3, X4)
U36_ga(X1, X2, qcD_out_gaaa(X1, X3, X4, X2)) → fibcF_out_ga(s(s(X1)), X2)
addcE_in_gga(0, 0, 0) → addcE_out_gga(0, 0, 0)
addcE_in_gga(s(X1), X2, s(X3)) → U34_gga(X1, X2, X3, addcE_in_gga(X1, X2, X3))
addcE_in_gga(X1, s(X2), s(X3)) → U35_gga(X1, X2, X3, addcE_in_gga(X1, X2, X3))
U34_gga(X1, X2, X3, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(s(X1), X2, s(X3))
U35_gga(X1, X2, X3, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(X1, s(X2), s(X3))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
fibcC_in_ga(x1, x2)  =  fibcC_in_ga(x1)
fibcC_out_ga(x1, x2)  =  fibcC_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
qcD_in_gaaa(x1, x2, x3, x4)  =  qcD_in_gaaa(x1)
U31_gaaa(x1, x2, x3, x4, x5)  =  U31_gaaa(x1, x5)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x2, x5)
fibcF_in_ga(x1, x2)  =  fibcF_in_ga(x1)
fibcF_out_ga(x1, x2)  =  fibcF_out_ga(x1, x2)
U36_ga(x1, x2, x3)  =  U36_ga(x1, x3)
qcD_out_gaaa(x1, x2, x3, x4)  =  qcD_out_gaaa(x1, x2, x3, x4)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x2, x3, x5)
addcE_in_gga(x1, x2, x3)  =  addcE_in_gga(x1, x2)
addcE_out_gga(x1, x2, x3)  =  addcE_out_gga(x1, x2, x3)
U34_gga(x1, x2, x3, x4)  =  U34_gga(x1, x2, x4)
U35_gga(x1, x2, x3, x4)  =  U35_gga(x1, x2, x4)
FIBC_IN_GA(x1, x2)  =  FIBC_IN_GA(x1)
PD_IN_GAAA(x1, x2, x3, x4)  =  PD_IN_GAAA(x1)
U6_GAAA(x1, x2, x3, x4, x5)  =  U6_GAAA(x1, x5)
FIBF_IN_GA(x1, x2)  =  FIBF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FIBC_IN_GA(s(X1)) → PD_IN_GAAA(X1)
PD_IN_GAAA(X1) → FIBC_IN_GA(X1)
PD_IN_GAAA(X1) → U6_GAAA(X1, fibcC_in_ga(X1))
U6_GAAA(X1, fibcC_out_ga(X1, X2)) → FIBF_IN_GA(X1)
FIBF_IN_GA(s(s(X1))) → PD_IN_GAAA(X1)

The TRS R consists of the following rules:

fibcC_in_ga(0) → fibcC_out_ga(0, s(0))
fibcC_in_ga(s(X1)) → U30_ga(X1, qcD_in_gaaa(X1))
U30_ga(X1, qcD_out_gaaa(X1, X3, X4, X2)) → fibcC_out_ga(s(X1), X2)
qcD_in_gaaa(X1) → U31_gaaa(X1, fibcC_in_ga(X1))
U31_gaaa(X1, fibcC_out_ga(X1, X2)) → U32_gaaa(X1, X2, fibcF_in_ga(X1))
U32_gaaa(X1, X2, fibcF_out_ga(X1, X3)) → U33_gaaa(X1, X2, X3, addcE_in_gga(X2, X3))
fibcF_in_ga(0) → fibcF_out_ga(0, 0)
fibcF_in_ga(s(0)) → fibcF_out_ga(s(0), s(0))
fibcF_in_ga(s(s(X1))) → U36_ga(X1, qcD_in_gaaa(X1))
U33_gaaa(X1, X2, X3, addcE_out_gga(X2, X3, X4)) → qcD_out_gaaa(X1, X2, X3, X4)
U36_ga(X1, qcD_out_gaaa(X1, X3, X4, X2)) → fibcF_out_ga(s(s(X1)), X2)
addcE_in_gga(0, 0) → addcE_out_gga(0, 0, 0)
addcE_in_gga(s(X1), X2) → U34_gga(X1, X2, addcE_in_gga(X1, X2))
addcE_in_gga(X1, s(X2)) → U35_gga(X1, X2, addcE_in_gga(X1, X2))
U34_gga(X1, X2, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(s(X1), X2, s(X3))
U35_gga(X1, X2, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(X1, s(X2), s(X3))

The set Q consists of the following terms:

fibcC_in_ga(x0)
U30_ga(x0, x1)
qcD_in_gaaa(x0)
U31_gaaa(x0, x1)
U32_gaaa(x0, x1, x2)
fibcF_in_ga(x0)
U33_gaaa(x0, x1, x2, x3)
U36_ga(x0, x1)
addcE_in_gga(x0, x1)
U34_gga(x0, x1, x2)
U35_gga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • PD_IN_GAAA(X1) → FIBC_IN_GA(X1)
    The graph contains the following edges 1 >= 1

  • PD_IN_GAAA(X1) → U6_GAAA(X1, fibcC_in_ga(X1))
    The graph contains the following edges 1 >= 1

  • FIBC_IN_GA(s(X1)) → PD_IN_GAAA(X1)
    The graph contains the following edges 1 > 1

  • FIBF_IN_GA(s(s(X1))) → PD_IN_GAAA(X1)
    The graph contains the following edges 1 > 1

  • U6_GAAA(X1, fibcC_out_ga(X1, X2)) → FIBF_IN_GA(X1)
    The graph contains the following edges 1 >= 1, 2 > 1

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDA_IN_GA(s(X1), s(X2)) → ADDA_IN_GA(X1, X2)

The TRS R consists of the following rules:

fibcH_in_a(0) → fibcH_out_a(0)
fibcC_in_ga(0, s(0)) → fibcC_out_ga(0, s(0))
fibcC_in_ga(s(X1), X2) → U30_ga(X1, X2, qcD_in_gaaa(X1, X3, X4, X2))
qcD_in_gaaa(X1, X2, X3, X4) → U31_gaaa(X1, X2, X3, X4, fibcC_in_ga(X1, X2))
U31_gaaa(X1, X2, X3, X4, fibcC_out_ga(X1, X2)) → U32_gaaa(X1, X2, X3, X4, fibcF_in_ga(X1, X3))
fibcF_in_ga(0, 0) → fibcF_out_ga(0, 0)
fibcF_in_ga(s(0), s(0)) → fibcF_out_ga(s(0), s(0))
fibcF_in_ga(s(s(X1)), X2) → U36_ga(X1, X2, qcD_in_gaaa(X1, X3, X4, X2))
U36_ga(X1, X2, qcD_out_gaaa(X1, X3, X4, X2)) → fibcF_out_ga(s(s(X1)), X2)
U32_gaaa(X1, X2, X3, X4, fibcF_out_ga(X1, X3)) → U33_gaaa(X1, X2, X3, X4, addcE_in_gga(X2, X3, X4))
addcE_in_gga(0, 0, 0) → addcE_out_gga(0, 0, 0)
addcE_in_gga(s(X1), X2, s(X3)) → U34_gga(X1, X2, X3, addcE_in_gga(X1, X2, X3))
addcE_in_gga(X1, s(X2), s(X3)) → U35_gga(X1, X2, X3, addcE_in_gga(X1, X2, X3))
U35_gga(X1, X2, X3, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(X1, s(X2), s(X3))
U34_gga(X1, X2, X3, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(s(X1), X2, s(X3))
U33_gaaa(X1, X2, X3, X4, addcE_out_gga(X2, X3, X4)) → qcD_out_gaaa(X1, X2, X3, X4)
U30_ga(X1, X2, qcD_out_gaaa(X1, X3, X4, X2)) → fibcC_out_ga(s(X1), X2)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
fibcH_in_a(x1)  =  fibcH_in_a
fibcH_out_a(x1)  =  fibcH_out_a(x1)
fibcC_in_ga(x1, x2)  =  fibcC_in_ga(x1)
fibcC_out_ga(x1, x2)  =  fibcC_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
qcD_in_gaaa(x1, x2, x3, x4)  =  qcD_in_gaaa(x1)
U31_gaaa(x1, x2, x3, x4, x5)  =  U31_gaaa(x1, x5)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x2, x5)
fibcF_in_ga(x1, x2)  =  fibcF_in_ga(x1)
fibcF_out_ga(x1, x2)  =  fibcF_out_ga(x1, x2)
U36_ga(x1, x2, x3)  =  U36_ga(x1, x3)
qcD_out_gaaa(x1, x2, x3, x4)  =  qcD_out_gaaa(x1, x2, x3, x4)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x2, x3, x5)
addcE_in_gga(x1, x2, x3)  =  addcE_in_gga(x1, x2)
addcE_out_gga(x1, x2, x3)  =  addcE_out_gga(x1, x2, x3)
U34_gga(x1, x2, x3, x4)  =  U34_gga(x1, x2, x4)
U35_gga(x1, x2, x3, x4)  =  U35_gga(x1, x2, x4)
ADDA_IN_GA(x1, x2)  =  ADDA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDA_IN_GA(s(X1), s(X2)) → ADDA_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ADDA_IN_GA(x1, x2)  =  ADDA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ADDA_IN_GA(s(X1)) → ADDA_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(33) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • ADDA_IN_GA(s(X1)) → ADDA_IN_GA(X1)
    The graph contains the following edges 1 > 1

(34) YES

(35) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDB_IN_GA(s(X1), s(X2)) → ADDB_IN_GA(X1, X2)

The TRS R consists of the following rules:

fibcH_in_a(0) → fibcH_out_a(0)
fibcC_in_ga(0, s(0)) → fibcC_out_ga(0, s(0))
fibcC_in_ga(s(X1), X2) → U30_ga(X1, X2, qcD_in_gaaa(X1, X3, X4, X2))
qcD_in_gaaa(X1, X2, X3, X4) → U31_gaaa(X1, X2, X3, X4, fibcC_in_ga(X1, X2))
U31_gaaa(X1, X2, X3, X4, fibcC_out_ga(X1, X2)) → U32_gaaa(X1, X2, X3, X4, fibcF_in_ga(X1, X3))
fibcF_in_ga(0, 0) → fibcF_out_ga(0, 0)
fibcF_in_ga(s(0), s(0)) → fibcF_out_ga(s(0), s(0))
fibcF_in_ga(s(s(X1)), X2) → U36_ga(X1, X2, qcD_in_gaaa(X1, X3, X4, X2))
U36_ga(X1, X2, qcD_out_gaaa(X1, X3, X4, X2)) → fibcF_out_ga(s(s(X1)), X2)
U32_gaaa(X1, X2, X3, X4, fibcF_out_ga(X1, X3)) → U33_gaaa(X1, X2, X3, X4, addcE_in_gga(X2, X3, X4))
addcE_in_gga(0, 0, 0) → addcE_out_gga(0, 0, 0)
addcE_in_gga(s(X1), X2, s(X3)) → U34_gga(X1, X2, X3, addcE_in_gga(X1, X2, X3))
addcE_in_gga(X1, s(X2), s(X3)) → U35_gga(X1, X2, X3, addcE_in_gga(X1, X2, X3))
U35_gga(X1, X2, X3, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(X1, s(X2), s(X3))
U34_gga(X1, X2, X3, addcE_out_gga(X1, X2, X3)) → addcE_out_gga(s(X1), X2, s(X3))
U33_gaaa(X1, X2, X3, X4, addcE_out_gga(X2, X3, X4)) → qcD_out_gaaa(X1, X2, X3, X4)
U30_ga(X1, X2, qcD_out_gaaa(X1, X3, X4, X2)) → fibcC_out_ga(s(X1), X2)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
fibcH_in_a(x1)  =  fibcH_in_a
fibcH_out_a(x1)  =  fibcH_out_a(x1)
fibcC_in_ga(x1, x2)  =  fibcC_in_ga(x1)
fibcC_out_ga(x1, x2)  =  fibcC_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
qcD_in_gaaa(x1, x2, x3, x4)  =  qcD_in_gaaa(x1)
U31_gaaa(x1, x2, x3, x4, x5)  =  U31_gaaa(x1, x5)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x2, x5)
fibcF_in_ga(x1, x2)  =  fibcF_in_ga(x1)
fibcF_out_ga(x1, x2)  =  fibcF_out_ga(x1, x2)
U36_ga(x1, x2, x3)  =  U36_ga(x1, x3)
qcD_out_gaaa(x1, x2, x3, x4)  =  qcD_out_gaaa(x1, x2, x3, x4)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x2, x3, x5)
addcE_in_gga(x1, x2, x3)  =  addcE_in_gga(x1, x2)
addcE_out_gga(x1, x2, x3)  =  addcE_out_gga(x1, x2, x3)
U34_gga(x1, x2, x3, x4)  =  U34_gga(x1, x2, x4)
U35_gga(x1, x2, x3, x4)  =  U35_gga(x1, x2, x4)
ADDB_IN_GA(x1, x2)  =  ADDB_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(36) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDB_IN_GA(s(X1), s(X2)) → ADDB_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ADDB_IN_GA(x1, x2)  =  ADDB_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(38) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ADDB_IN_GA(s(X1)) → ADDB_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(40) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • ADDB_IN_GA(s(X1)) → ADDB_IN_GA(X1)
    The graph contains the following edges 1 > 1

(41) YES